Inference at * 1 1 1 
Iof proof for Lemma fun with inv is bij:



1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. (g o f) = Id{A}
6. (f o g) = Id{B}
7. a1 : A
8. a2 : A
9. f(a1) = f(a2)
  a1 = a2 

latex

 by ((ApplyFunToHypEquands g 9) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 10. g(f(a1)) = g(f(a2))
C1:   a1 = a2
C.

Definitions

x:AB(x), s = t